es:ES, i:Id, P:(discrete state@i).
@i stable state.P(state)  
 e@i. P((discrete state after e))  (e':E. (e <loc e')  P((discrete state when e'))) 

latex

Definitions	{T}, SQType(T), x. t(x), True, T, t  T, e@i. P(e), x(s), P  Q, , x:A. B(x), P  Q, e'e.P(e'), (e <loc e'), P  Q, P & Q
Lemmas	es-le-pred, es-pred wf, stable-implies2, es-loc-pred, Id sq, es-locl-iff, dstate-after-pred, event system wf, Id wf, es-stable wf, es-loc wf, true wf, squash wf, es-dstate wf, es-dstate-after wf, es-E wf, es-locl wf